Nuprl Lemma : assert-es-eq-E-2
11,40
postcript
pdf
the_es
:ES,
e
,
e'
:E. (
e
=
e'
)
(
e
=
e'
)
latex
Definitions
Type
,
EqDecider(
T
)
,
x
:
A
B
(
x
)
,
EOrderAxioms(
E
;
pred?
;
info
)
,
val-axiom(
E
;
V
;
M
;
info
;
pred?
;
init
;
Trans
;
Choose
;
Send
;
val
;
time
)
,
x
:
A
.
B
(
x
)
,
Top
,
s
=
t
,
P
Q
,
P
Q
,
x
:
A
B
(
x
)
,
P
&
Q
,
P
Q
,
,
t
T
,
eqof(
d
)
,
f
(
a
)
,
b
,
E
,
e
=
e'
,
ES
Lemmas
es-E
wf
,
event
system
wf
,
iff
functionality
wrt
iff
,
deq
property
,
iff
wf
,
rev
implies
wf
,
assert
wf
,
eqof
wf
origin
the_es:ES, e, e':E. (
e = e') 
(e = e') the_es:ES, e, e':E. (e = e') (e = e') 
B(x)x:A. B(x) Q Q
B(x) Q
Tb